perm filename PFAC.NEW[P,JRA] blob
sn#106944 filedate 1974-12-09 generic text, type T, neo UTF8
00100 (THVSETQ (THV ULS) T)
00200 (CSYM AV000)
00300 (THVSETQ (THV ANS) (LIST (LIST (QUOTE THV) (GENSYM))))
00400 (THVSET (CAR (THV ANS)) NIL)
00500
00600
00700 (THVSETQ (THV WF) NIL)
00800 (THVSETQ (THV GCTR) 0)
00900 (THVSETQ (THV UF) NIL)
01000 (THVSETQ (THV XN) 0)
01100 (THVSETQ (THV ZN) 0)
01200 (THVSETQ (THV YN) 0)
01300 (THVSETQ (THV COMMENTLIST) NIL)
01400 (THVSETQ (THV PLANL) NIL)
01500 (THVSETQ (THV ASSL) NIL)
01600 (THVSETQ (THV PASSUM) NIL)
01700 (SETQ GTEMP NIL)
01800 (SETQ CT NIL)
01900 (SETQ BTSW NIL)
02000 (THVSETQ (THV DG) NIL)
02100 (SETQ AL NIL)
02200 (SETQ AN 0)
02300 (SETQ SRULES (QUOTE (((MINUS (PLUS X Y) Y) X)((SUB1(ADD1 X))X) ((DIV (PROD X Y) Y) X))))
02400 (SETQ SSW NIL)
02500 (SETQ FIFOL NIL)
02600 (SETQ LIFOL NIL)
02700 (SETQ SN 0)
02800 (SETQ PN 0)
02900 (SETQ READY NIL)
03000 (SETQ UNCERTLIST NIL)
03100 (THVSETQ (THV DBLITS) NIL)
03200 (THVSETQ (THV ASSERTLITS) NIL)
03300 (SETQ JOINCOND NIL)
03400
03500
03600 (THVSETQ (THV PROCLIST) NIL)
03700 (THVSETQ (THV PROCDATA) NIL)
03800
03900
04000 (THASSERT (ISVAR X0))
04100 (THASSERT (VFACT (1) (1) R))
04200 (THASSERT (INTEGER N))
04300
04400
04500 (THVSETQ (THV CFACTARGS) NIL)
04600 (THVSETQ (THV CFACTINST) NIL)
04700
04800 (DEFPROP CFACTGREMLIN (THERASING (V3 V4) (CFACT (THV V3) (THV V4) R) (THCOND ((MEMBER (THV CFACTINST) (THV CFACT~
04900 ARGS)) (THASSERT (WRONG PATH))))) THEOREM)
05000
05100 (THASSERT CFACTGREMLIN)
05200
05300 (THVSETQ (THV NCFACTARGS) NIL)
05400 (THVSETQ (THV NCFACTINST) NIL)
05500
05600 (DEFPROP NCFACTGREMLIN (THERASING (V3 V4) (NCFACT (THV V3) (THV V4) R) (THCOND ((MEMBER (THV NCFACTINST) (THV NC~
05700 FACTARGS)) (THASSERT (WRONG PATH))))) THEOREM)
05800
05900 (THASSERT NCFACTGREMLIN)
06000
06100 (THVSETQ (THV =ARGS) NIL)
06200 (THVSETQ (THV =INST) NIL)
06300
06400 (DEFPROP =GREMLIN (THERASING (V6 V2) (= (THV V6) (THV V2) R) (THCOND ((MEMBER (THV =INST) (THV =ARGS)) (THASSERT~
06500 (WRONG PATH))))) THEOREM)
06600
06700 (THASSERT =GREMLIN)
06800
06900 (THVSETQ (THV N=ARGS) NIL)
07000 (THVSETQ (THV N=INST) NIL)
07100
07200 (DEFPROP N=GREMLIN (THERASING (V6 V2) (N= (THV V6) (THV V2) R) (THCOND ((MEMBER (THV N=INST) (THV N=ARGS)) (THAS~
07300 SERT (WRONG PATH))))) THEOREM)
07400
07500 (THASSERT N=GREMLIN)
07600
07700 (THVSETQ (THV CARGS) NIL)
07800 (THVSETQ (THV CINST) NIL)
07900
08000 (DEFPROP CGREMLIN (THERASING (V4 V6) (C (THV V4) (THV V6) R) (THCOND ((MEMBER (THV CINST) (THV CARGS)) (THASSERT~
08100 (WRONG PATH))))) THEOREM)
08200
08300 (THASSERT CGREMLIN)
08400
08500 (THVSETQ (THV NCARGS) NIL)
08600 (THVSETQ (THV NCINST) NIL)
08700
08800 (DEFPROP NCGREMLIN (THERASING (V4 V6) (NC (THV V4) (THV V6) R) (THCOND ((MEMBER (THV NCINST) (THV NCARGS)) (THAS~
08900 SERT (WRONG PATH))))) THEOREM)
09000
09100 (THASSERT NCGREMLIN)
09200
09300 (THVSETQ (THV CPRODARGS) NIL)
09400 (THVSETQ (THV CPRODINST) NIL)
09500
09600 (DEFPROP CPRODGREMLIN (THERASING (V1 V2 V3) (CPROD (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV CPRODINST~
09700 ) (THV CPRODARGS)) (THASSERT (WRONG PATH))))) THEOREM)
09800
09900 (THASSERT CPRODGREMLIN)
10000
10100 (THVSETQ (THV NCPRODARGS) NIL)
10200 (THVSETQ (THV NCPRODINST) NIL)
10300
10400 (DEFPROP NCPRODGREMLIN (THERASING (V1 V2 V3) (NCPROD (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV NCPRODI~
10500 NST) (THV NCPRODARGS)) (THASSERT (WRONG PATH))))) THEOREM)
10600
10700 (THASSERT NCPRODGREMLIN)
10800
10900 (THVSETQ (THV VFACTARGS) NIL)
11000 (THVSETQ (THV VFACTINST) NIL)
11100
11200 (DEFPROP VFACTGREMLIN (THERASING ((DIV V9 V10) (SUB1 V10)) (VFACT (THV DIV) (THV SUB1) R) (THCOND ((MEMBER (THV ~
11300 VFACTINST) (THV VFACTARGS)) (THASSERT (WRONG PATH))))) THEOREM)
11400
11500 (THASSERT VFACTGREMLIN)
11600
11700 (THVSETQ (THV NVFACTARGS) NIL)
11800 (THVSETQ (THV NVFACTINST) NIL)
11900
12000 (DEFPROP NVFACTGREMLIN (THERASING ((DIV V9 V10) (SUB1 V10)) (NVFACT (THV DIV) (THV SUB1) R) (THCOND ((MEMBER (TH~
12100 V NVFACTINST) (THV NVFACTARGS)) (THASSERT (WRONG PATH))))) THEOREM)
12200
12300 (THASSERT NVFACTGREMLIN)
12400
12500 (THVSETQ (THV PRODUCTARGS) NIL)
12600 (THVSETQ (THV PRODUCTINST) NIL)
12700
12800 (DEFPROP PRODUCTGREMLIN (THERASING ((MINUS V5 V3) (SUB1 V6) V3) (PRODUCT (THV MINUS) (THV SUB1) (THV V3) R) (THC~
12900 OND ((MEMBER (THV PRODUCTINST) (THV PRODUCTARGS)) (THASSERT (WRONG PATH))))) THEOREM)
13000
13100 (THASSERT PRODUCTGREMLIN)
13200
13300 (THVSETQ (THV NPRODUCTARGS) NIL)
13400 (THVSETQ (THV NPRODUCTINST) NIL)
13500
13600 (DEFPROP NPRODUCTGREMLIN (THERASING ((MINUS V5 V3) (SUB1 V6) V3) (NPRODUCT (THV MINUS) (THV SUB1) (THV V3) R) (T~
13700 HCOND ((MEMBER (THV NPRODUCTINST) (THV NPRODUCTARGS)) (THASSERT (WRONG PATH))))) THEOREM)
13800
13900 (THASSERT NPRODUCTGREMLIN)
14000
14100
14200
14300 (SETQ RTTAPROD NIL)
14400 (SETQ RFTAPROD NIL)
14500 (DEFPROP TAPROD
14600 (THCONSE (CGL V6 V5 V3 (LSTTAPROD (QUOTE (V3 V6 V5))))
14700 (PRODUCT (THV V5) (THV V6) (THV V3) R)
14800 (THSETQ (THV LCTR) (THV GCTR))
14900 (SETQ THME (ADD1 THME))
15000 (TREEPATH TAPROD (PRODUCT (THV V5) (THV V6) (THV V3) R))
15100 (TRACEINFO1)
15200 (THOR T (TRACEINFO2 TAPROD))
15300 (COND ((TTYIN) (ADVICESYS)) (T T))
15400 (THOR (THAND (THCOND ((THASVAL (THV V5)) (EQUAL (THV V5) (QUOTE (0))))
15500 (T (THSETQ (THV V5) (QUOTE (0)))))
15600 (THCOND ((THASVAL (THV V6)) (EQUAL (THV V6) (QUOTE (0))))
15700 (T (THSETQ (THV V6) (QUOTE (0))))))
15800 (THGOAL (PRODUCT (THEV (LIST (QUOTE MINUS) (THV V5) (THV V3)))
15900 (THEV (LIST (QUOTE SUB1) (THV V6)))
16000 (THV V3)
16100 R)
16200 (THTBF FILTEROP))
16300 (CONDSTAT (THV CGL) T))
16400 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
16500 (SETQ THMS (ADD1 THMS))
16600 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
16700 THEOREM)
16800
16900
17000 (SETQ RTTAFACT NIL)
17100 (SETQ RFTAFACT NIL)
17200 (DEFPROP TAFACT
17300 (THCONSE (CGL V10 V9 (LSTTAFACT (QUOTE (V10 V9))))
17400 (VFACT (THV V9) (THV V10) R)
17500 (THSETQ (THV LCTR) (THV GCTR))
17600 (SETQ THME (ADD1 THME))
17700 (TREEPATH TAFACT (VFACT (THV V9) (THV V10) R))
17800 (TRACEINFO1)
17900 (THOR T (TRACEINFO2 TAFACT))
18000 (COND ((TTYIN) (ADVICESYS)) (T T))
18100 (THGOAL (VFACT (THEV (LIST (QUOTE DIV) (THV V9) (THV V10)))
18200 (THEV (LIST (QUOTE SUB1) (THV V10)))
18300 R)
18400 (THTBF FILTEROP))
18500 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
18600 (SETQ THMS (ADD1 THMS))
18700 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
18800 THEOREM)
18900
19000
19100 (SETQ RTTPROD NIL)
19200 (SETQ RFTPROD NIL)
19300 (DEFPROP TPROD
19400 (THCONSE (INASS NAMES V2 V3 V5 V6 V1 V4 D1 FT NT CGL LCTR LWF LUF PS PB BP SASSERTLITS INVAR1 INVAR2 CTST)
19500 (CPROD (THV V1) (THV V2) (THV V3) R)
19600 (THSETQ (THV LCTR) (THV GCTR))
19700 (SETQ THME (ADD1 THME))
19800 (TREEPATH TPROD (CPROD (THV V1) (THV V2) (THV V3) R))
19900 (TRACEINFO1)
20000 (THOR T (TRACEINFO2 TPROD))
20100 (COND ((TTYIN) (ADVICESYS)) (T T))
20200 (THSETQ (THV LWF) NIL T T)
20300 (THCOND ((NOT (THV WF)) (THSETQ (THV LWF) T)) (T T))
20400 (THSETQ (THV WF) T)
20500 (THSETQ (THV LUF) NIL T T)
20600 (THSETQ (THV PS) (EVAL (CAR (THV ANS))) T T)
20700 (THDO (THVSET (CAR (THV ANS)) NIL))
20800 (NEWVAR (THV V4))
20900 (THGOAL (C (THV V4) (0) R) (THTBF FILTEROP))
21000 (THCOND ((THAND (THASVAL (THV V4)))
21100 (THSETQ (THV CARGS) (CONS (LIST (THV V4) (QUOTE (0))) (THV CARGS))))
21200 (T T))
21300 (THGOAL (C (THV V1) (0) R) (THTBF FILTEROP))
21400 (THCOND ((THAND (THASVAL (THV V1)))
21500 (THSETQ (THV CARGS) (CONS (LIST (THV V1) (QUOTE (0))) (THV CARGS))))
21600 (T T))
21700 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
21800 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
21900 (THSETQ (THV BP) (EVAL (CAR (THV ANS))) T T)
22000 (THDO (THVSET (CAR (THV ANS)) NIL))
22100 (THOR T (THFAIL THEOREM))
22200 REP
22300 (THGOAL (C (THV V4) (THV V6) R) (THTBF FILTERAX))
22400 (THGOAL (C (THV V1) (THV V5) R) (THTBF FILTERAX))
22500 (THGOAL (PRODUCT (THV V5) (THV V6) (THV V3) R) (THTBF FILTERAX))
22600
22700 (THSETQ(THV INASS)(LIST (THV V1)(THV V2)(THV V3)(THV V4)
22800 (THV V5)(THV V6)) T T)
22900 (THSETQ(THV NAMES)(LIST @V1 @V2 @V3 @V4 @V5 @V6)T T)
23000 (THASSERT (C Y4 Y6 R))
23100 (THASSERT (C Y1 Y5 R))
23200 (THASSERT (ISVAR Y1))
23300 (THASSERT (ISVAR Y4))
23400 (THASSERT (PRODUCT Y5 Y6 Y3 R))
23500
23600 (THSETQ (THV CTST) (LIST (QUOTE =) (THV V6) (THV V2)))
23700 (THOR T (THFAIL THEOREM))
23800 (THSETQ (THV SASSERTLITS) (THV ASSERTLITS) T T)
23900
24000 (THGOAL(C Y4(ADD1 Y6) R) (THTBF FILTEROP))
24100 (THGOAL(C Y1(PLUS Y5 Y3)R)(THTBF FILTEROP))
24200 (THASSERT(C (THV V4)(THEV(LIST(QUOTE ADD1)(THV V6)))R))
24300 (THASSERT(C(THV V1)(THEV(LIST(QUOTE PLUS)(THV V5)(THV V3)))R))
24400 (THSETQ (THV INVAR1)(QUOTE
24500 ((C Z4 Z6)(C Z1 Z5)(PRODUCT Z5 Z6 Z3))) T T)
24600
24700
24800 (THSETQ (THV V5) (QUOTE THUNASSIGNED))
24900 (THSETQ (THV V6) (QUOTE THUNASSIGNED))
25000 (THGOAL (C (THV V4) (THV V6) R) (THTBF FILTERAX))
25100 (THGOAL (C (THV V1) (THV V5) R) (THTBF FILTERAX))
25200 (THGOAL (PRODUCT (THV V5) (THV V6) (THV V3) R) (THTBF FILTERAX))
25300 (THSETQ (THV PB) (EVAL (CAR (THV ANS))) T T)
25400 (SETQ GTEMP
25500 (WHILASSEM (THV BP)
25600 (THV PB)
25700 (CONS(THV NAMES)(THV INASS))
25800 (THV INVAR1)
25900 (THV CTST)))
26000 (THSETQ (THV PB) GTEMP T T)
26100 (THSETQ (THV PLANL)
26200 (CONS (LIST (LIST (QUOTE PROD) (THV V1) (THV V2) (THV V3)) (THV PB)) (THV PLANL)))
26300 (THCOND ((THV LWF) (THSET (CAR (THV ANS)) (APPEND (THV PB) (THV PS))))
26400 (T
26500 (THSET (CAR (THV ANS))
26600 (APPEND
26700 (LIST (LIST (QUOTE ←) (THV V1) (LIST (QUOTE PROD) (THV V2) (THV V3))))))))
26800 (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THSETQ (THV CINST) (LIST (THV V1) (THV D1))))
26900 (T T))
27000 (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THERASE (C (THV V1) (THV D1) R) (THTBF THTRUE)))
27100 (T T))
27200 (THCOND ((THERASE (WRONG PATH)) (THFAIL THEOREM)) (T T))
27300 (THASSERT (C (THV V1) (THEV (LIST (QUOTE PROD) (THV V2) (THV V3))) R))
27400 (THSETQ (THV ASSERTLITS)
27500 (CONS (PRINT(LIST (LIST (QUOTE C)
27600 (THV V1)
27700 (LIST (QUOTE PROD) (THV V2) (THV V3))
27800 (QUOTE R))
27900 (LIST (QUOTE A) (QUOTE A))))
28000 (THV ASSERTLITS)))
28100 (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
28200 (THCOND ((THV LWF) (THSETQ (THV WF) NIL T T)
28300 (THSETQ (THV BT) NIL T T)
28400 (SETQ GANS (REMBT GANS)))
28500 (T T))
28600 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
28700 (THCOND ((THV LUF) (THSETQ (THV UF) NIL T T)) (T T))
28800 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
28900 THEOREM)
29000
29100
29200 (SETQ RTTFACT NIL)
29300 (SETQ RFTFACT NIL)
29400 (DEFPROP TFACT
29500 (THCONSE (INASS NAMES V1 V2 V9 V10 V3 V6 V5 V4 V7 V8 FT NT CGL LCTR LWF LUF PS PB BP SASSERTLITS INVAR1 INVAR2 CTST)
29600 (CFACT (THV V3) (THV V4) R)
29700 (THSETQ (THV LCTR) (THV GCTR))
29800 (SETQ THME (ADD1 THME))
29900 (TREEPATH TFACT (CFACT (THV V3) (THV V4) R))
30000 (TRACEINFO1)
30100 (THOR T (TRACEINFO2 TFACT))
30200 (COND ((TTYIN) (ADVICESYS)) (T T))
30300
30400 (THSETQ(THV V1) NIL T T)
30500 (THSETQ(THV V2) NIL T T)
30600 (THSETQ(THV V8) NIL T T)
30700
30800 (THSETQ (THV LWF) NIL T T)
30900 (THCOND ((NOT (THV WF)) (THSETQ (THV LWF) T)) (T T))
31000 (THSETQ (THV WF) T)
31100 (THSETQ (THV LUF) NIL T T)
31200 (THSETQ (THV PS) (EVAL (CAR (THV ANS))) T T)
31300 (THDO (THVSET (CAR (THV ANS)) NIL))
31400 (THGOAL (INTEGER (THV V4)))
31500 (NEWVAR (THV V7))
31600 (THGOAL (VFACT (THV V5) (THV V6) R) (THTBF FILTEROP))
31700 (THCOND
31800 ((THAND (THASVAL (THV V6)) (THASVAL (THV V5)))
31900 (THSETQ (THV VFACTARGS) (CONS (LIST (THV V5) (THV V6)) (THV VFACTARGS))))
32000 (T T))
32100 (THGOAL (C (THV V3) (THV V5) R) (THTBF FILTEROP))
32200 (THCOND ((THAND (THASVAL (THV V5)) (THASVAL (THV V3)))
32300 (THSETQ (THV CARGS) (CONS (LIST (THV V3) (THV V5)) (THV CARGS))))
32400 (T T))
32500 (THGOAL (C (THV V7) (THV V6) R) (THTBF FILTEROP))
32600 (THCOND ((THAND (THASVAL (THV V6)) (THASVAL (THV V7)))
32700 (THSETQ (THV CARGS) (CONS (LIST (THV V7) (THV V6)) (THV CARGS))))
32800 (T T))
32900 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
33000 (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
33100 (THCOND ((NULL (THV VFACTARGS)) T) (T (THSETQ (THV VFACTARGS) (CDR (THV VFACTARGS)) T T)))
33200 (THSETQ (THV BP) (EVAL (CAR (THV ANS))) T T)
33300 (THDO (THVSET (CAR (THV ANS)) NIL))
33400 (THOR T (THFAIL THEOREM))
33500 REP
33600 (THGOAL (C (THV V7) (THV V10) R) (THTBF FILTERAX))
33700 (THGOAL (C (THV V3) (THV V9) R) (THTBF FILTERAX))
33800 (THGOAL (VFACT (THV V9) (THV V10) R) (THTBF FILTERAX))
33900
34000 (THSETQ(THV INASS)(LIST (THV V1)(THV V2)(THV V3)(THV V4)
34100 (THV V5)(THV V6)(THV V7)(THV V8)(THV V9)(THV V10)) T T)
34200 (THSETQ(THV NAMES)(LIST @V1 @V2 @V3 @V4 @V5 @V6 @V7 @V8 @V9 @V10)T T)
34300 (THASSERT (C Y7 Y10 R))
34400 (THASSERT(C Y3 Y9 R))
34500 (THASSERT(VFACT Y9 Y10 R))
34600 (THASSERT(ISVAR Y7))
34700 (THASSERT(ISVAR Y3))
34800
34900
35000 (THSETQ (THV CTST) (LIST (QUOTE >) (THV V10) (THV V4)))
35100 (THOR T (THFAIL THEOREM))
35200 (THSETQ (THV SASSERTLITS) (THV ASSERTLITS) T T)
35300
35400 (THGOAL (C Y7 (ADD1 Y10)R)(THTBF FILTEROP))
35500 (THGOAL (CPROD Y3 Y9 (ADD1 Y10)R)(THTBF FILTEROP))
35600 (THASSERT(C(THV V7)(THEV(LIST (QUOTE ADD1)(THV V10)))R))
35700 (THASSERT(CPROD (THV V3)(THV V9)(THEV (LIST (QUOTE ADD1)(THV V10)))R))
35800 (THSETQ (THV INVAR1)(QUOTE
35900 ((C Z7 Z10)(C Z3 Z9)(VFACT Z9 Z10)))T T)
36000
36100 (THSETQ (THV V9) (QUOTE THUNASSIGNED))
36200 (THSETQ (THV V10) (QUOTE THUNASSIGNED))
36300 (THGOAL (C (THV V7) (THV V10) R) (THTBF FILTERAX))
36400 (THGOAL (C (THV V3) (THV V9) R) (THTBF FILTERAX))
36500 (PRINT @YEP)(PRINT (THV V3))(PRINT(THV V7))
36600 (THGOAL (VFACT (THV V9) (THV V10) R) (THTBF FILTERAX))
36700 (THSETQ (THV PB) (EVAL (CAR (THV ANS))) T T)
36800
36900 (SETQ GTEMP
37000 (WHILASSEM (THV BP)
37100 (THV PB)
37200 (CONS(THV NAMES)(THV INASS))
37300 (THV INVAR1)
37400 (THV CTST)))
37500 (THSETQ (THV PB) GTEMP T T)
37600 (THSET (CAR (THV ANS)) (APPEND (THV PB) (THV PS)))
37700 (THASSERT (FACT (THV V3) (THV V4) R))
37800 (THSETQ (THV ASSERTLITS)
37900 (CONS (LIST (LIST (QUOTE FACT) (THV V3) (THV V4) (QUOTE R))
38000 (LIST (QUOTE A) (QUOTE A)))
38100 (THV ASSERTLITS)))
38200 (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
38300 (THCOND ((THV LWF) (THSETQ (THV WF) NIL T T)
38400 (THSETQ (THV BT) NIL T T)
38500 (SETQ GANS (REMBT GANS)))
38600 (T T))
38700 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
38800 (THCOND ((THV LUF) (THSETQ (THV UF) NIL T T)) (T T))
38900 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
39000 THEOREM)
39100
39200
39300 (SETQ RT← NIL)
39400 (SETQ RF← NIL)
39500 (DEFPROP ←
39600 (THCONSE (CGL A1 V1 D1 (LST← (QUOTE (A1 V1))))
39700 (C (THV V1) (THV A1) R)
39800 (THSETQ (THV LCTR) (THV GCTR))
39900 (SETQ THME (ADD1 THME))
40000 (THUNIQUE LST←)
40100 (TREEPATH ← (C (THV V1) (THV A1) R))
40200 (TRACEINFO1)
40300 (THOR T (TRACEINFO2 ←))
40400 (COND ((TTYIN) (ADVICESYS)) (T T))
40500 (THGOAL (ISVAR (THV V1)))
40600 (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THSETQ (THV CINST) (LIST (THV V1) (THV D1))))
40700 (T T))
40800 (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THERASE (C (THV V1) (THV D1) R) (THTBF THTRUE)))
40900 (T T))
41000 (THCOND ((THERASE (WRONG PATH)) (THFAIL THEOREM)) (T T))
41100 (THSET (CAR (THV ANS))
41200 (CONS (CONS (QUOTE ←) (LIST (THV V1) (THV A1))) (EVAL (CAR (THV ANS)))))
41300 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
41400 (SETQ THMS (ADD1 THMS))
41500 (THASSERT (C (THV V1) (THV A1) R))
41600 (THSETQ (THV ASSERTLITS)
41700 (CONS (LIST (LIST (QUOTE C) (THV V1) (THV A1) (QUOTE R)) (LIST (QUOTE A) (QUOTE A)))
41800 (THV ASSERTLITS)))
41900 (PRINT (REVERSE (EVAL (CAR (THV ANS)))))
42000 (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
42100 (COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
42200 (THDO (TERPRI))
42300 (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
42400 THEOREM)
42500
42600
42700 (THASSERT ←)
42800
42900
43000 (THASSERT TFACT)
43100
43200
43300 (THASSERT TPROD)
43400
43500
43600 (THASSERT TAFACT)
43700
43800
43900 (THASSERT TAPROD)
44000 (DEFPROP RESTOREPROP
44100 (LAMBDA NIL
44200 (PROG NIL
44300 (SETQ STAT T)
44400 (SETQ FUNDEFLIST
44500 (QUOTE
44600 ((ADD1 (X) (/( X /+ 1 /))) (SUB1 (X) (/( X /- 1 /))) (PLUS (X Y) (/( X /+ Y /))))))
44700 (PUTPROP (QUOTE PRODUCT) T (QUOTE DEF))
44800 (PUTPROP (QUOTE PRODUCT) (QUOTE NIL) (QUOTE UNIQ))
44900 (PUTPROP (QUOTE PRODUCT) (QUOTE NIL) (QUOTE UNCERT))
45000 (PUTPROP (QUOTE PRODUCT) (QUOTE NIL) (QUOTE PARTIAL))
45100 (PUTPROP (QUOTE PRODUCT) (QUOTE T) (QUOTE FLUENT))
45200 (PUTPROP (QUOTE FACT) T (QUOTE DEF))
45300 (PUTPROP (QUOTE FACT) (QUOTE NIL) (QUOTE UNIQ))
45400 (PUTPROP (QUOTE FACT) (QUOTE NIL) (QUOTE UNCERT))
45500 (PUTPROP (QUOTE FACT) (QUOTE NIL) (QUOTE PARTIAL))
45600 (PUTPROP (QUOTE FACT) (QUOTE T) (QUOTE FLUENT))
45700 (PUTPROP (QUOTE VFACT) T (QUOTE DEF))
45800 (PUTPROP (QUOTE VFACT) (QUOTE NIL) (QUOTE UNIQ))
45900 (PUTPROP (QUOTE VFACT) (QUOTE NIL) (QUOTE UNCERT))
46000 (PUTPROP (QUOTE VFACT) (QUOTE NIL) (QUOTE PARTIAL))
46100 (PUTPROP (QUOTE VFACT) (QUOTE T) (QUOTE FLUENT))
46200 (PUTPROP (QUOTE CFACT) T (QUOTE DEF))
46300 (PUTPROP (QUOTE CFACT) (QUOTE NIL) (QUOTE UNIQ))
46400 (PUTPROP (QUOTE CFACT) (QUOTE NIL) (QUOTE UNCERT))
46500 (PUTPROP (QUOTE CFACT) (QUOTE NIL) (QUOTE PARTIAL))
46600 (PUTPROP (QUOTE CFACT) (QUOTE T) (QUOTE FLUENT))
46700 (PUTPROP (QUOTE CPROD) T (QUOTE DEF))
46800 (PUTPROP (QUOTE CPROD) (QUOTE NIL) (QUOTE UNIQ))
46900 (PUTPROP (QUOTE CPROD) (QUOTE NIL) (QUOTE UNCERT))
47000 (PUTPROP (QUOTE CPROD) (QUOTE NIL) (QUOTE PARTIAL))
47100 (PUTPROP (QUOTE CPROD) (QUOTE T) (QUOTE FLUENT))
47200 (PUTPROP (QUOTE =) T (QUOTE DEF))
47300 (PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE UNIQ))
47400 (PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE UNCERT))
47500 (PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE PARTIAL))
47600 (PUTPROP (QUOTE =) (QUOTE T) (QUOTE FLUENT))
47700 (PUTPROP (QUOTE INTEGER) T (QUOTE DEF))
47800 (PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE UNIQ))
47900 (PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE UNCERT))
48000 (PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE PARTIAL))
48100 (PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE FLUENT))
48200 (PUTPROP (QUOTE >) T (QUOTE DEF))
48300 (PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE UNIQ))
48400 (PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE UNCERT))
48500 (PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE PARTIAL))
48600 (PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE FLUENT))
48700 (PUTPROP (QUOTE C) T (QUOTE DEF))
48800 (PUTPROP (QUOTE C) (QUOTE (X *)) (QUOTE UNIQ))
48900 (PUTPROP (QUOTE C) (QUOTE NIL) (QUOTE UNCERT))
49000 (PUTPROP (QUOTE C) (QUOTE NIL) (QUOTE PARTIAL))
49100 (PUTPROP (QUOTE C) (QUOTE T) (QUOTE FLUENT))
49200 (PUTPROP (QUOTE TAPROD) (QUOTE NIL) (QUOTE INEQ))
49300 (PUTPROP (QUOTE TAPROD) (QUOTE T) (QUOTE REC))
49400 (PUTPROP (QUOTE TAPROD) (QUOTE NIL) (QUOTE ASSUM))
49500 (PUTPROP (QUOTE TAPROD) (QUOTE NIL) (QUOTE ARG))
49600 (PUTPROP (QUOTE TAPROD) T (QUOTE AX))
49700 (PUTPROP (QUOTE TAFACT) (QUOTE NIL) (QUOTE INEQ))
49800 (PUTPROP (QUOTE TAFACT) (QUOTE T) (QUOTE REC))
49900 (PUTPROP (QUOTE TAFACT) (QUOTE NIL) (QUOTE ASSUM))
50000 (PUTPROP (QUOTE TAFACT) (QUOTE NIL) (QUOTE ARG))
50100 (PUTPROP (QUOTE TAFACT) T (QUOTE AX))
50200 (PUTPROP (QUOTE TPROD) (QUOTE NIL) (QUOTE INEQ))
50300 (PUTPROP (QUOTE TPROD) (QUOTE NIL) (QUOTE REC))
50400 (PUTPROP (QUOTE TPROD) (QUOTE NIL) (QUOTE ASSUM))
50500 (PUTPROP (QUOTE TPROD) (QUOTE NIL) (QUOTE ARG))
50600 (PUTPROP (QUOTE TPROD) T (QUOTE ITER))
50700 (PUTPROP (QUOTE TFACT) (QUOTE NIL) (QUOTE INEQ))
50800 (PUTPROP (QUOTE TFACT) (QUOTE NIL) (QUOTE REC))
50900 (PUTPROP (QUOTE TFACT) (QUOTE NIL) (QUOTE ASSUM))
51000 (PUTPROP (QUOTE TFACT) (QUOTE NIL) (QUOTE ARG))
51100 (PUTPROP (QUOTE TFACT) T (QUOTE ITER))
51200 (PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE INEQ))
51300 (PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE REC))
51400 (PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE ASSUM))
51500 (PUTPROP (QUOTE ←) (QUOTE (V1 A1)) (QUOTE ARG))
51600 (PUTPROP (QUOTE ←) T (QUOTE OP))))
51700 EXPR)